{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main (main) where

import Control.Lens ( view, set )
import Data.List (intercalate)
import Data.Version (showVersion)
import System.Environment (lookupEnv)
import System.Exit (exitFailure)
import System.FilePath (splitSearchPath)
import System.IO (hPutStrLn, stderr)
import Options.Applicative
    ( Parser,
      Alternative((<|>)),
      help,
      hidden,
      infoOption,
      long,
      metavar,
      short,
      strOption,
      value )

import CryptolServer.Check ( check, checkDescr )
import CryptolServer.CheckDocstrings ( checkDocstringsAPI, checkDocstringsDescr )
import CryptolServer.ClearState
    ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr)
import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
import CryptolServer.Interrupt
    ( interruptServer, interruptServerDescr )
import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
import Cryptol.TypeCheck.AST (tcTopEntitytName, ImpName(..))
import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName)
import Cryptol.Utils.Logger (quietLogger)
import Cryptol.Version (displayVersionStr)
import qualified Paths_cryptol_remote_api as RPC

import Argo (AppMethod, mkApp, defaultAppOpts, StateMutability(PureState))
import Argo.DefaultMain ( customMain, userOptions )
import qualified Argo.Doc as Doc


import CryptolServer
    ( ServerState, moduleEnv, tcSolver, initialState, extendSearchPath, command, notification )
import CryptolServer.Call ( call )
import CryptolServer.Data.Expression ( Expression )
import CryptolServer.Data.Type ( JSONSchema )
import CryptolServer.EvalExpr (evalExpressionDescr, evalExpression)
import CryptolServer.ExtendSearchPath (extSearchPath, extSearchPathDescr)
import CryptolServer.FocusedModule (focusedModuleDescr, focusedModule)
import CryptolServer.FocusModule (focusModule, focusModuleDescr)
import CryptolServer.Names ( visibleNamesDescr, visibleNames )
import CryptolServer.Modules ( visibleModulesDescr, visibleModules )
import CryptolServer.TypeCheck ( checkType )
import CryptolServer.Sat ( proveSatDescr, proveSat )
import Cryptol.REPL.Command (CommandResult, DocstringResult)

main :: IO ()
main = customMain initMod initMod initMod initMod versionParser description buildApp
  where
    buildApp opts =
      mkApp
        "Cryptol RPC Server"
        evalServerDocs
        (defaultAppOpts PureState)
        (startingState (userOptions opts))
        cryptolEvalMethods

    startingState (StartingFile file) reader =
      do paths <- getSearchPaths
         initSt <- extendSearchPath paths <$> initialState
         let s    = view tcSolver initSt
         let menv = view moduleEnv initSt
         let minp = ModuleInput {
                      minpCallStacks = False,
                      minpSaveRenamed = False,
                      minpEvalOpts = pure evOpts,
                      minpByteReader = reader,
                      minpModuleEnv = menv,
                      minpTCSolver = s
         }
         let die =
               \err ->
                 do hPutStrLn stderr $ "Failed to load " ++ either ("file " ++) (("module " ++) . show) file ++ ":\n" ++ show err
                    exitFailure
         menv' <-
           do (res, _warnings) <- either loadModuleByPath loadModuleByName file minp
              -- NB Warnings suppressed when running server
              case res of
                Left err -> die err
                Right (m, menv') ->
                  do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (ImpTop (tcTopEntitytName (snd m))))
                     case res' of
                       Left err -> die err
                       Right (_, menv'') -> pure menv''
         return $ set moduleEnv menv' initSt

    evOpts =
      EvalOpts { evalLogger = quietLogger
               , evalPPOpts = defaultPPOpts
               }


evalServerDocs :: [Doc.Block]
evalServerDocs =
  [ Doc.Section "Summary" $ [ Doc.Paragraph
    [Doc.Text "A remote server for ",
     Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
     Doc.Text " that supports only type checking and evaluation of Cryptol code."]]
  , Doc.Section "Terms and Types"
    [Doc.datatype @Expression,
     Doc.datatype @JSONSchema,
     Doc.datatype @DocstringResult,
     Doc.datatype @CommandResult]
  ]

description :: String
description =
  "An RPC server for Cryptol that supports only type checking and evaluation of Cryptol code."

getSearchPaths :: IO [FilePath]
getSearchPaths =
  maybe [] splitSearchPath <$> lookupEnv "CRYPTOLPATH"

newtype StartingFile =
  StartingFile (Either FilePath ModName)

initMod :: Parser StartingFile
initMod = StartingFile <$> (Left <$> filename <|> Right . textToModName <$> modulename)
  where
    filename =
      strOption $
      long "file" <>
      metavar "FILENAME" <>
      help "Cryptol file to load on startup"
    modulename =
      strOption $
      long "module" <>
      metavar "MODULE" <>
      help "Cryptol module to load on startup" <>
      value (modNameToText preludeName)

-- | Display the version number when the @--version@/@-v@ option is supplied.
versionParser :: Parser (a -> a)
versionParser =
  infoOption versionStr $
  mconcat
    [ long "version"
    , short 'v'
    , help "Display version number"
    , hidden
    ]
  where
    versionStr :: String
    versionStr =
      intercalate "\n"
        [ "Cryptol RPC server " ++ showVersion RPC.version
        , displayVersionStr
        ]

cryptolEvalMethods :: [AppMethod ServerState]
cryptolEvalMethods =
  [ command
    "check"
    checkDescr
    check
  , command
     "focused module"
     focusedModuleDescr
     focusedModule
  , command
     "focus module"
     focusModuleDescr
     focusModule
  , command
     "evaluate expression"
     evalExpressionDescr
     evalExpression
  , command
     "extend search path"
     extSearchPathDescr
     extSearchPath
  , command
     "call"
     (Doc.Paragraph [Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."])
     call
  , command
     "visible names"
     visibleNamesDescr
     visibleNames
  , command
     "visible modules"
     visibleModulesDescr
     visibleModules
  , command
     "check type"
     (Doc.Paragraph [Doc.Text "Check and return the type of the given expression."])
     checkType
  , command
     "prove or satisfy"
     proveSatDescr
     proveSat
  , notification
    "clear state"
    clearStateDescr
    clearState
  , notification
    "clear all states"
    clearAllStatesDescr
    clearAllStates
  , command
     "check docstrings"
     checkDocstringsDescr
     checkDocstringsAPI
  , notification
     "interrupt"
     interruptServerDescr
     interruptServer
  ]
